COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	declare PREDPAR F 1,INDVAR X
C00003 ENDMK
C⊗;
declare PREDPAR F 1,INDVAR X;

axiom induction: F(0)∧∀X.(F(X)⊃F(X+1)) ⊃ ∀X.F(X);;